5.7 KB · ⇊ 4 parts · ⤓ Micron 5.7 KB · ⤓ HTML 30.9 KB

top

In formal reasoning, in particular in mathematical logic, computer algebra, and automated theorem proving, a fresh variable is a variable that did not occur in the context considered so far.cite-ref-1[1] The concept is often used without explanation.cite-ref-2[2]

Fresh variables may be used to replace other variables, to eliminate variable shadowing or capture. For instance, in alpha-conversion, the processing of terms in the lambda calculus into equivalent terms with renamed variables, replacing variables with fresh variables can be helpful as a way to avoid accidentally capturing variables that should be free.cite-ref-3[3] Another use for fresh variables involves the development of loop invariants in formal program verification, where it is sometimes useful to replace constants by newly introduced fresh variables.cite-ref-4[4]

• Example

• Notes

• References

For example, in term rewriting, before applying a rule l → → r {\displaystyle l\to r} to a given term t {\displaystyle t} , each variable in l → → r {\displaystyle l\to r} should be replaced by a fresh one to avoid clashes with variables occurring in t {\displaystyle t} . Given the rule

a p p e n d ( c o n s ( x , y ) , z ) → → c o n s ( x , a p p e n d ( y , z ) ) {\displaystyle append(cons(x,y),z)\to cons(x,append(y,z))}

and the term

a p p e n d ( c o n s ( x , c o n s ( y , n i l ) ) , c o n s ( 3 , n i l ) ) {\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))} ,

attempting to find a matching substitution of the rule's left-hand side, a p p e n d ( c o n s ( x , y ) , z ) {\displaystyle append(cons(x,y),z)} , within a p p e n d ( c o n s ( x , c o n s ( y , n i l ) ) , c o n s ( 3 , n i l ) ) {\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))} will fail, since y {\displaystyle y} cannot match c o n s ( y , n i l ) {\displaystyle cons(y,nil)} . However, if the rule is replaced by a fresh copycite-ref-copy-5-0[a]

a p p e n d ( c o n s ( v 1 , v 2 ) , v 3 ) → → c o n s ( v 1 , a p p e n d ( v 2 , v 3 ) ) {\displaystyle append(cons(v_{1},v_{2}),v_{3})\to cons(v_{1},append(v_{2},v_{3}))}

before, matching will succeed with the answer substitution { v 1 ↦ ↦ x , v 2 ↦ ↦ c o n s ( y , n i l ) , v 3 ↦ ↦ c o n s ( 3 , n i l ) } {\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto cons(y,nil),\;v_{3}\mapsto cons(3,nil)\}} .

cite-note-copy-5a. ↑ that is, a copy with each variable consistently replaced by a fresh variable

cite-note-11. ↑ citerefcarmen-bruni2018Carmen Bruni (2018). Predicate Logic: Natural Deduction (PDF) (Lecture Slides). Univ. of Waterloo. Here: slide 13/26.

cite-note-22. ↑ citerefmichael-f-rber2023Michael Färber (Feb 2023). Denotational Semantics and a Fast Interpreter for jq (Technical Report). Univ. of Innsbruck. arXiv:2302.10576. Here: p.4.

cite-note-33. ↑ citerefgordonmelham1996Gordon, Andrew D.; Melham, Thomas F. (1996). "Five axioms of alpha-conversion". In von Wright, Joakim; Grundy, Jim; Harrison, John (eds.). Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings. Lecture Notes in Computer Science. Vol. 1125. Springer. pp. 173–190. doi:10.1007/BFB0105404. ISBN 978-3-540-61587-3.

cite-note-44. ↑ citerefcohen1990Cohen, Edward (1990). "Loops B — On replacing constants by fresh variables". Programming in the 1990s. Monographs in Computer Science. New York: Springer. pp. 149–194. doi:10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID 1509875.